Lean 4 マクロ
Lean 4 マクロ
code:hs
/- Declares a parser -/
syntax (priority := high) "{" term,+ "}" : term
/- Declares two expansions/syntax transformers -/
macro_rules
| ({$x}) => (Set.singleton $x)
| ({$x, $xs:term,*}) => (Set.insert $x {$xs,*})
関連
メモ
調査用